COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(
C00016 ENDMK
C⊗;
(
HELP
"This program is designed to be used as a tool for verification
of properties of PASCAL programs presented to it, along with
lemmas about those programs.  The most commonly used upper level
command is PARSE.  Type (DHELP WHAT) for a list of help commands.
For help on topic X, assuming help data exists, type (DHELP X)."

WHAT
"DHELP messages are available for the following:
ALIAS
BUG
DOCUMENTATION
DUMPINTERNAL
DUMPSYMBOLS
DUMPRULE
DUMPVC
LISP
LOADSYMBOLS
LOADRULE
LOADVC
MANUAL
PARSE
PREVIOUS
PRINTVC
READVC
SIMPINIT
SIMPLIFY
VC
This file (which contains all the help routines) is NEWVER.HLP[1,3].
"
ALIAS
"This command is used to change the default disk area used by DUMPVC,
DUMPRULE, LOADVC, and LOADRULE.  (ALIAS (EX VER)), for example, will
set [EX,VER] as the default area for these commands.  Of course, you
can override the default by specifying the area explicitly in one
of these commands.  (ALIAS) will display your current default area.
The PARSE and READVC commands may or may not be affected by ALIAS.
This should change shortly."

BUG
"The BUG feature is provided to help verifier hackers make changes
to syntax, semantics, etc.  There are two user commands,
(SETBUG <number>) and (RESETBUG <number>), which set and then reset
the bug with the appropriate number.  See MEMO[VCG,RAK] to see which
bugs currently exist and what they do."

DOCUMENTATION
"Files intended to be documentation on the verifier or portions 
thereof are kept in the directory [DOC,VER].  You might try looking
there for things.  Don't be too surprised if some large gaps exist.

Here are a few other random places:
MEMO[VCG,RAK] about the parser, Pascal, etc.
SSEM[VCG,RAK] --page 2 explains the structure of the symbol table
VERIFY.DOC[DOC,VER]--details about LOADVC, LOADRULE, DUMPVC, DUMPRULE,
	ALIAS.   Also information about examples in EX,VER, hackery
	information, etc.
"

DUMPINTERNAL
"This command is either (DUMPINTERNAL T) or (DUMPINTERNAL NIL) to
turn the facility on or off; default is NIL.  DUMPINTERNAL causes
internal format output by the parser to be placed in the symbol
table for each procedure or function parsed.  It is generally only
useful in conjunction with dumping the symbol table (see DUMPSYMBOLS)
and the VC command (see VC)."

DUMPRULE
"The command DUMPRULE is used to dump a 'compiled' rulefile to disk.
It allows use of the standalone simplifier, VPROVE, and also saves
parse time because rulefiles need only be parsed once, then dumped.
The default filename is VERIFY.CRL in you aliased area.  The ALIAS
command affects DUMPRULE and LOADRULE.   This command should 
be used in conjunction with LOADRULE, which loads these 'compiled'
rulefiles.   Thus, you can parse a rulefile using VCGEN or VERIFY, 
do a DUMPRULE, and then load it via LOADRULE into either VPROVE 
or VERIFY.    Examples:  (DUMPRULE (SORT)) makes SORT.CRL.
(DUMPRULE (FOO CRL (VER BAR))) makes FOO.CRL[VER,BAR].   If more than
one rulefile exists, it will dump the most recent one parsed.  You may
also specify a rulefile name to DUMPRULE, as in (DUMPRULE (SORT) SORTRULES).
LOADRULE is used to load in these files.  Example: (LOADRULE (FOO))
reads in FOO.CRL.  (LOADRULE) reads in VERIFY.CRL."

DUMPSYMBOLS
"The command DUMPSYMBOLS is optionally followed by a file in the
same format as PARSE.  It instructs the parser to dump code to that
file that will permit reloading the symbol table environment of all
the procedures in the file.  (DUMPSYMBOLS) turns off dumping.  So
does any subsequent attempt to load a symbol table file.  See
LOADSYMBOLS for information on how to load a symbol table."

DUMPVC
"The command DUMPVC is used to dump verification conditions into
a file.   It is usefule because it allows use of the standalone prover,
VPROVE, and because it saves parsing time by storing the VCs in their
internal format.   The default filename for dumped VCs is VERIFY.CVC
in your aliased area.   DUMPVC is affected by the ALIAS command, as is
LOADVC, its counterpart.  LOADVC is used to load these files.   Thus,
a program may be parsed with VCGEN or VERIFY, and the VCs dumped with 
DUMPVC.  The LOADVC may be used to load the VCs into VPROVE or VERIFY
for later use.   Examples:  (DUMPVC (FOO)) puts the compiled VCs
into FOO.CVC in your aliased area.   (DUMPVC (FOO CVC (VER BAR)))
puts them in FOO.CVC[VER,BAR].  LOADVC has a corresponding syntax:
(LOADVC (FOO)) reads in FOO.CVC; (LOADVC) reads in VERIFY.CVC."

LISP
"Although this is primarily a program verifier, it exists in a
MACLSP environment.  This means that the general facilities of
such LISP are available.   The file VERIFY.DOC[DOC,VER] contains
some advice about recovery from errors, etc. in MACLISP."

LOADRULE
"The command LOADRULE is used to load in files created with DUMPRULE.
See DUMPRULE for further information."

LOADSYMBOLS
"The command LOADSYMBOLS must be followed by two items: first a
procedure name and then a file.  The system will turn off symbol
table dumping (if it is on), clear the symbol table, and then attempt
to load the symbol table environment of the procedure specified from
the file given.  The format of the file name is the same as that of
the PARSE command. See DUMPSYMBOLS for information on how to create
a file that contains symbol table information."

LOADVC
"The command LOADVC is used to load in files created by DUMPVC.
See DUMPVC for further information."

MANUAL
"Unfortunately, manual mode is not up yet.  If you want to
implement it, talk to WLS."
 
PARSE
"The command (PARSE) accepts input from the teletype. (PARSE X)
will try to take input from the file X.  Here are some examples
for taking files with two word names and from another directory
(here p,pn is programmer,project and X Y is the two word file name
X.Y): (PARSE X Y), (PARSE X (P,PN)), and (PARSE X Y (P,PN))  .  
The parser calls the verification condition generator, but does
not do simplification.  For this, the command SIMPLIFY must be
used. The syntactic scan and semantic routines should NEVER
bomb out, no matter what string you give them.  If they do,
send a note to RAK and SAVE the program!!!"

PREVIOUS
"The command (PREVIOUS <positive integer>) has meaning when a
syntax scan finds a syntax error.  It will print out as many
tokens preceding the syntax error as it is asked (if there are
that many).  (PREVIOUS 10) is called in the errorhandling.  As
the number of tokens requested increases, time to find them can
go up alarmingly. After an error and before parsing something
else, previous may be called as many times as desired."

PRINTVC
"The command PRINTVC is used to output unsimplified verfication
conditions.  (PRINTVC) prints out all of these on the
terminal.  (PRINTVC X) prints out all of the VC's for procedure
X.  (PRINTVC X 3) prints the third VC for procedure X.
(PRINTVC (F)) prints out all VC's to file F, which is replaced
if it was previously present.  (PRINTVC (F) X) prints out all
VC's for procedure X on file F.
The outer block of a program is currently called MAIN. It will
remove VC's for a procedure named MAIN, if one is present!"

READVC
"The command READVC is used to input verification conditions in
external format that were dumped by either a PRINTVC, SIMPLIFY,
or RESIMPLIFY command.  READVC takes a file name in the same
format as PARSE.   It will expect that file to be a list of
VCs in external format as output by the system.  All previously
existing VCs are deleted and all VCs in the file are loaded.
Note that you may use READVC to continue from a partially
simplified VC dumped by SIMPLIFY.  When used from the terminal,
READVC expects a list of one or more of the form NAME VC,
terminated by a period.  It is probably best to enclose the 
last VC in parenthesis, as the final period is frequently
mistaken for a record -field indicator."


SIMPINIT
"The SIMPINIT command is used to reinitialize the simplifier.  It
should be called whenever a simplification has terminated incorrectly,
for example, in a breakpoint.   In MACLISP, incant <control>G to 
escape from a breakpoint.   In general use, you will never have to do
(SIMPINIT)."

SIMPLIFY
"The command SIMPLIFY is used to call the simplifier and output
simplified verification conditions.  The procedure and output
file specifications are the same as for PRINTVC.  Use
(HELP PRINTVC) to see these conventions."

VC
"This command is not intended for general use.
(VC @procname) sets up and calls the verification condition generator.
It requires that the name be a procedue or function, with internal
format dumped by the parser.  This dumping usually requires that
DUMPINTERNAL be set (which see) when parsing the procedure."

END
)